A, B:Type. (A r B)  (MaInterface(A) r MaInterface(B)) 

latex

Definitions	Type, t  T, Atom$n, Id, x:A. B(x), Top, P  Q, left + right, x:AB(x), State(ds), x.A(x), x. t(x), x:A  B(x), Knd, b, {x:A| B(x)} , a:A fp B(a), True, T, type List, (x  l), S  T, hasloc(k;i), s = t, a < b, #$n, ||as||, Void, False, A, A  B, , , l[i], A c B, MaInterface(T)
Lemmas	Id wf, l member wf, nat wf, length wf1, select wf, Knd wf, assert wf, hasloc wf, decl-state wf, fpf wf, squash wf, true wf, subtype-fpf2, subtype rel product, subtype rel function, top wf, subtype rel sum, subtype rel self